Extend lub/glb to more types by ggreif · Pull Request #340 · caffeinelabs/motoko

ggreif · 2019-04-23T19:51:05Z

This is a peek at the final version and request for comment on the further direction.

Added to the type algebra:

tuples
objects
arrays
functions
Shared
futures

Laundry list:

This is somewhat restricted w.r.t. polymorphism: * only monomorphic functions are allowed * can we come up with a mapping scheme for tyvars (alpha equivalence?) Further, sharing and control modes must match. Former could be relaxed, possibly.

rossberg

Yes, there are quite a few more cases, just follow the cases for subtyping.

src/type.ml

ggreif · 2019-04-24T13:52:22Z

test/fail/ok/type-inference.tc.ok

  ()
 false produces
  {}
-type-inference.as:13.9-13.53: warning, this if has type Any because branches have inconsistent types,


Since we can now lub/glb fields, this former top-level Any now appears inside of the object type. I suggest to make this warning visible again, by recursively examining the resulting type. This is probably tricky.

I don't follow, the lub of () and {} should still be Any?

That line is

let _ = if true (new {x = 5}) else (new {var x = 5});

no idea why the error message used to mention () !?

ActorScript 0.1 interpreter > new {var x = 5}; {x = 5} : {x : var Nat} > new {x = 5}; {x = 5} : {x : Nat}

That is very odd? Does that test really succeed on master?

You are looking at the wrong lines. The diff shows in red what is gone. That part is consistent.

Ah, okay, phew, that makes more sense.

In that case, the warning is gone. That's fine, I don't see what else would make sense.

However, I just realised that our handling of var vs subtyping may not be what we want -- because it is second-class, var T should probably be an isolated point in the subtype lattice, not a sub/supertype of Any/None (though I think that's still sound given our current representation of mutable arrays). But then you'd need special handling of var arrays and var fields, e.g., the lub of the above should be {}. May not worth it.

Maybe worth getting rid of VarT t and instead making it a boolean flag on ArrayT and the exp_field?

I am handling the Mut t very cautiously, and e.g. have now:

$ ./asc ActorScript 0.1 interpreter > [[var 42],[25]]; [[42], [25]] : [[Any]]

Which should probably be [[42], [25]] : [[Int]].

No, [Int] is not a supertype of [var Int], that would be incorrect. As subtyping is defined right now, it must be Any. But that subtyping probably is a mistake in itself, I plan to change that -- but you can ignore that for now.

ggreif · 2019-04-24T18:25:40Z

EDIT: Resolved!

@rossberg I have added some instrumentation, such that when sub t u returns true, I check that lub t u equals u. (Will do the dual with glb). Now I see problems:

bad LUB: Non -> Nat     ({len : () -> Nat} -> Nat     <:     Text -> Nat) 
bad LUB: Non -> Nat     ({len : () -> Nat} -> Nat     <:     [Int] -> Nat)

~~Maybe the subtype check is too lenient here?~~

EDIT: ~~It is!~~ It uses

rel_list rel_typ rel eq (List.map (open_ ts) t21) (List.map (open_ ts) t11)

for local functions, i.e. it doesn't consider the specialness of Text and [T] w.r.t. glb. (Actually it is not in that business!)

nomeata · 2019-04-24T18:57:36Z

Are you saying that <: is wrong? But {len : () -> Nat} -> Nat <: Text -> Nat is true and sound.

And indeed I would expect

   lub ({len : () -> Nat} -> Nat) (Text -> Nat)
= (glb {len : () -> Nat} Text) (lub Nat Nat)
= Text -> Nat

and glb {len : () -> Nat} Text = Text is, I think, is what Andreas meant with

the glb of an Array and another Obj must be an Array at most. Similarly for Text.

Below Text there is only Non, so you can simply implement glb as

glb Text t = if Text <: t then Text else Non

ggreif · 2019-04-24T19:26:47Z

Are you saying that <: is wrong? But {len : () -> Nat} -> Nat <: Text -> Nat is true and sound.

And indeed I would expect
   lub ({len : () -> Nat} -> Nat) (Text -> Nat)
= (glb {len : () -> Nat} Text) (lub Nat Nat)
= Text -> Nat
and glb {len : () -> Nat} Text = Text is, I think, is what Andreas meant with

the glb of an Array and another Obj must be an Array at most. Similarly for Text.

Below Text there is only Non, so you can simply implement glb as
glb Text t = if Text <: t then Text else Non

I have implemented that rule, no idea why it doesn't trigger. Let me check. (Back from walking the dog in a dust storm, phew!)

Addendum: Indeed I had it wrong! In 2 of 4 lines I had the comparison backwards.

ggreif · 2019-04-24T20:39:55Z

Next finding: Recursive objects send the current object lub into an infinite recursion. E.g.

type A = {x : A};
type B = {x : B};
func f(x : A) : A = x : B;

(I'll conjecture that recursive variants will do the same. I'll add tests.)
I think we'll need some memoizing lub/glb to survive recursive tests.

rossberg · 2019-04-25T06:58:14Z

Recursive objects send the current object lub into an infinite recursion.

Now that you mention it I remember the effort in handling this properly was the main reason why I hadn't implemented full lub/glb right away. :) But I think you can follow the pattern from rel_typ.

WIP: preserve insert loop-breakers when there is danger of creating value recursion WIP: handle Variant, Tup and Array WIP: first cleanups WIP: add predicate to test for loop breaker Con more cleanups too WIP: trying to understand the crash prelude:200.1-225.2: internal error, Stack overflow Raised by primitive operation at file "check_ir.ml", line 149, characters 14-29 Called from file "list.ml", line 100, characters 12-15 WIP: actually return the potential loop-breaker recursive function types and Async with tests further cleanups

ggreif · 2019-05-06T07:53:46Z

Recursive objects send the current object lub into an infinite recursion.

Now that you mention it I remember the effort in handling this properly was the main reason why I hadn't implemented full lub/glb right away. :) But I think you can follow the pattern from rel_typ.

e67d424 is a first attempt to control recursive type inputs. It is not yet in final form, feel free to comment on the acceptability of the lazy approach with eventual strict mixup of OCaml objects.

Oh, and please ignore the changes of function identifiers with primes (e.g. lub', etc.), as these are going away when I remove the instrumentation for the sub <--> {lub, glb} consistency checks.

ggreif

Handling Mut is the only open question. ~~Apart from the suggested lazy mechanics, which are admittedly gross, but all other alternatives I have considered are worse.~~
Update: The only effect base I make use of now is the rewriting of Con kinds, as done in other places too.

src/type.ml

ggreif · 2019-05-06T08:40:09Z

src/type.ml

+  | Tup' of typ list Lazy.t                   (* tuple *)
+  | Func' of sharing * control * bind list * typ list Lazy.t * typ list Lazy.t  (* function *)
+  | Async' of typ Lazy.t                      (* future *)
+  (*| Mut' of typ Lazy.t                         mutable type *)


Mutable fields (of Obj, Array) are tricky. I am punting on them for now.

src/type.ml

rossberg

Hm... I don't understand why we need all this laziness and loop breaker stuff. It should suffice to create a new Def con (which essentially is a mu) when you encounter one (or two). You initialise it with type Pre and update it on the way back. In all cases where neither of the two types is a Def con you do not need to do anything special.

@rossberg

This avoids editing typ' (at the cost of creating slightly bigger typ structures in the heap) but is totally worth it. No more laziness or recursive value objects needed. Follows @rossberg's suggestion in review. Remaining problems are mostly parametrised `Func` related: --- type-inclusion.run-low (expected) +++ type-inclusion.run-low (actual) @@ -0,0 +1,112 @@ +bad LUB: Any (<X>X -> X <: <Y <: Nat>Y -> Y) +bad GLB: Non (<X>X -> X <: <Y <: Nat>Y -> Y) ...

ggreif · 2019-05-06T16:13:55Z

Hm... I don't understand why we need all this laziness and loop breaker stuff. It should suffice to create a new Def con (which essentially is a mu) when you encounter one (or two). You initialise it with type Pre and update it on the way back. In all cases where neither of the two types is a Def con you do not need to do anything special.

Cool idea! I had the lingering intuition that rewriting the kind of a Con could solve the recursion problem, but I had the mechanism of rec and lazy mostly working when I added Con as µ-surrogates. I did not do rewriting because I had a good pointer to the result due to laziness.

This solution probably conses more (by creating bigger cycles), but recursive types are rare anyway.

Have a look at ed10d51, it should do what you suggest.

ggreif added 7 commits April 23, 2019 13:30

fix nits

950293e

reorder clauses

e16f88b

add tests

96972a7

implement lub/glb for objects

0691fc8

implement Tup and Array

63e3220

implement function type lub/glb

5365bf9

This is somewhat restricted w.r.t. polymorphism: * only monomorphic functions are allowed * can we come up with a mapping scheme for tyvars (alpha equivalence?) Further, sharing and control modes must match. Former could be relaxed, possibly.

check via REPL that correct types are inferred

f05be0c

ggreif requested review from nomeata and rossberg April 23, 2019 20:06

rossberg reviewed Apr 24, 2019

View reviewed changes

src/type.ml Outdated Show resolved Hide resolved

src/type.ml Outdated Show resolved Hide resolved

src/type.ml Outdated Show resolved Hide resolved

ggreif added 3 commits April 24, 2019 14:37

account for Text and Array not having proper Obj subtypes

e0fe75a

exercise glb for variants

1e0b8d2

Allow polymorphic functions, alpha-equiv still lacking

4e31d50

ggreif commented Apr 24, 2019

View reviewed changes

lub/glb for shared

32a82b4

ggreif added 2 commits April 24, 2019 21:50

fix thinko

f473d10

WIP: lub/glb for Var

72196df

ggreif commented May 6, 2019

View reviewed changes

rossberg reviewed May 6, 2019

View reviewed changes

ggreif added 2 commits May 6, 2019 16:33

add documentation and more clean-ups

66151b7

remove newline

77b4482

Conversation

ggreif commented Apr 23, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ggreif Apr 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ggreif commented Apr 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Apr 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ggreif commented Apr 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ggreif commented Apr 24, 2019

Uh oh!

rossberg commented Apr 25, 2019

Uh oh!

ggreif commented May 6, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ggreif left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

ggreif commented May 6, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

ggreif commented Apr 23, 2019 •

edited

Loading

ggreif Apr 24, 2019 •

edited

Loading

ggreif commented Apr 24, 2019 •

edited

Loading

nomeata commented Apr 24, 2019 •

edited

Loading

ggreif commented Apr 24, 2019 •

edited

Loading

ggreif commented May 6, 2019 •

edited

Loading

ggreif left a comment •

edited

Loading